use std::collections::HashSet;
use std::fmt;

/// 逻辑事实
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct Fact {
    pub predicate: String,
    pub arguments: Vec<String>,
}

impl Fact {
    pub fn new(predicate: impl Into<String>, arguments: Vec<String>) -> Self {
        Fact {
            predicate: predicate.into(),
            arguments,
        }
    }
}

impl fmt::Display for Fact {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}({})", self.predicate, self.arguments.join(", "))
    }
}

/// 逻辑规则: premises -> conclusion
#[derive(Debug, Clone)]
pub struct Rule {
    pub name: String,
    pub premises: Vec<Fact>,
    pub conclusion: Fact,
    pub confidence: f64, // 规则的置信度
}

impl Rule {
    pub fn new(
        name: impl Into<String>,
        premises: Vec<Fact>,
        conclusion: Fact,
        confidence: f64,
    ) -> Self {
        Rule {
            name: name.into(),
            premises,
            conclusion,
            confidence: confidence.clamp(0.0, 1.0),
        }
    }
}

impl fmt::Display for Rule {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let premises_str = self
            .premises
            .iter()
            .map(|p| p.to_string())
            .collect::<Vec<_>>()
            .join(" ∧ ");
        write!(
            f,
            "{}: {} -> {} (confidence: {:.2})",
            self.name, premises_str, self.conclusion, self.confidence
        )
    }
}

/// 符号推理引擎
#[derive(Debug, Clone)]
pub struct SymbolicEngine {
    facts: HashSet<Fact>,
    rules: Vec<Rule>,
    inference_log: Vec<String>,
}

impl SymbolicEngine {
    /// 创建新的符号引擎
    pub fn new() -> Self {
        SymbolicEngine {
            facts: HashSet::new(),
            rules: Vec::new(),
            inference_log: Vec::new(),
        }
    }

    /// 添加事实
    pub fn add_fact(&mut self, fact: Fact) {
        self.facts.insert(fact);
    }

    /// 添加规则
    pub fn add_rule(&mut self, rule: Rule) {
        self.rules.push(rule);
    }

    /// 检查事实是否存在
    pub fn has_fact(&self, fact: &Fact) -> bool {
        self.facts.contains(fact)
    }

    /// 获取所有事实
    pub fn get_facts(&self) -> Vec<&Fact> {
        self.facts.iter().collect()
    }

    /// 获取推理日志
    pub fn get_inference_log(&self) -> &[String] {
        &self.inference_log
    }

    /// 清除推理日志
    pub fn clear_log(&mut self) {
        self.inference_log.clear();
    }

    /// 前向链式推理
    pub fn forward_chain(&mut self, max_iterations: usize) -> usize {
        let mut new_facts_count = 0;
        self.inference_log.clear();

        for iteration in 0..max_iterations {
            let mut new_facts = Vec::new();

            // 尝试应用每条规则
            for rule in &self.rules {
                // 检查所有前提是否满足
                let all_premises_satisfied = rule.premises.iter().all(|premise| {
                    self.facts.contains(premise)
                });

                // 如果前提满足且结论还不存在,则推导出新事实
                if all_premises_satisfied && !self.facts.contains(&rule.conclusion) {
                    new_facts.push((rule.conclusion.clone(), rule.confidence, rule.name.clone()));
                }
            }

            // 如果没有新事实,停止推理
            if new_facts.is_empty() {
                self.inference_log.push(format!(
                    "推理终止于第 {} 轮,共推导出 {} 个新事实",
                    iteration + 1,
                    new_facts_count
                ));
                break;
            }

            // 添加新事实
            for (fact, confidence, rule_name) in new_facts {
                self.facts.insert(fact.clone());
                new_facts_count += 1;
                let log = format!(
                    "第 {} 轮: 通过规则 '{}' 推导出 {} (置信度: {:.2})",
                    iteration + 1,
                    rule_name,
                    fact,
                    confidence
                );
                self.inference_log.push(log);
            }
        }

        new_facts_count
    }

    /// 后向链式推理(目标驱动)
    pub fn backward_chain(&mut self, goal: &Fact) -> bool {
        self.inference_log.clear();
        self.backward_chain_helper(goal, 0)
    }

    fn backward_chain_helper(&mut self, goal: &Fact, depth: usize) -> bool {
        let indent = "  ".repeat(depth);

        // 如果目标已经是已知事实
        if self.facts.contains(goal) {
            self.inference_log.push(format!("{}✓ {} 已知", indent, goal));
            return true;
        }

        self.inference_log.push(format!("{}? 尝试证明 {}", indent, goal));

        // 查找可以推导出目标的规则
        for rule in self.rules.clone() {
            if rule.conclusion == *goal {
                self.inference_log.push(format!(
                    "{}  使用规则: {}",
                    indent, rule.name
                ));

                // 递归尝试证明所有前提
                let mut all_satisfied = true;
                for premise in &rule.premises {
                    if !self.backward_chain_helper(premise, depth + 1) {
                        all_satisfied = false;
                        break;
                    }
                }

                if all_satisfied {
                    // 所有前提都满足,添加目标为新事实
                    self.facts.insert(goal.clone());
                    self.inference_log.push(format!(
                        "{}✓ 成功推导 {} (置信度: {:.2})",
                        indent, goal, rule.confidence
                    ));
                    return true;
                }
            }
        }

        self.inference_log.push(format!("{}✗ 无法证明 {}", indent, goal));
        false
    }

    /// 查询满足条件的事实
    pub fn query(&self, predicate: &str) -> Vec<&Fact> {
        self.facts
            .iter()
            .filter(|f| f.predicate == predicate)
            .collect()
    }

    /// 解释推理路径
    pub fn explain(&self, fact: &Fact) -> Option<String> {
        if self.facts.contains(fact) {
            Some(format!("事实 {} 存在于知识库中", fact))
        } else {
            None
        }
    }
}

impl Default for SymbolicEngine {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_symbolic_reasoning() {
        let mut engine = SymbolicEngine::new();

        // 添加事实
        engine.add_fact(Fact::new("animal", vec!["cat".to_string()]));
        engine.add_fact(Fact::new("has_fur", vec!["cat".to_string()]));

        // 添加规则: animal(X) ∧ has_fur(X) -> mammal(X)
        engine.add_rule(Rule::new(
            "mammal_rule",
            vec![
                Fact::new("animal", vec!["cat".to_string()]),
                Fact::new("has_fur", vec!["cat".to_string()]),
            ],
            Fact::new("mammal", vec!["cat".to_string()]),
            0.95,
        ));

        // 前向推理
        let count = engine.forward_chain(10);
        assert_eq!(count, 1);
        assert!(engine.has_fact(&Fact::new("mammal", vec!["cat".to_string()])));
    }
}

